Motivated by the problem of verifying the correctness of arrhythmia-detectionalgorithms, we present a formalization of these algorithms in the language ofQuantitative Regular Expressions. QREs are a flexible formal language forspecifying complex numerical queries over data streams, with provable runtimeand memory consumption guarantees. The medical-device algorithms of interestinclude peak detection (where a peak in a cardiac signal indicates a heartbeat)and various discriminators, each of which uses a feature of the cardiac signalto distinguish fatal from non-fatal arrhythmias. Expressing these algorithms'desired output in current temporal logics, and implementing them via monitorsynthesis, is cumbersome, error-prone, computationally expensive, and sometimesinfeasible. In contrast, we show that a range of peak detectors (in both the time andwavelet domains) and various discriminators at the heart of today'sarrhythmia-detection devices are easily expressible in QREs. The fact that oneformalism (QREs) is used to describe the desired end-to-end operation of anarrhythmia detector opens the way to formal analysis and rigorous testing ofthese detectors' correctness and performance. Such analysis could alleviate theregulatory burden on device developers when modifying their algorithms. Theperformance of the peak-detection QREs is demonstrated by running them on realpatient data, on which they yield results on par with those provided by acardiologist.
展开▼
